; RUN: %solver --unconstrained-variable-elimination=0 %s | %OutputCheck %s
; CHECK-NEXT: ^sat

(push 1)
(set-info :source | fuzzsmt 0.3 |)
(set-logic  QF_ABV)
(set-info :status unknown)
(declare-fun v238684 () (_ BitVec 3))
(declare-fun v238685 () (_ BitVec 3))
(declare-fun v238686 () (_ BitVec 3))
(declare-fun a238687 () (Array (_ BitVec 8) (_ BitVec 13)))
(declare-fun a238688 () (Array (_ BitVec 9) (_ BitVec 6)))
(assert
(let ((e238689 (_ bv4206 14)))
(let ((e238690 (_ bv100 13)))
(let ((e238691 (ite (= (_ bv1 1) ((_ extract 0 0) e238690)) v238684 v238685)))
(let ((e238692 (bvor v238686 e238691)))
(let ((e238693 ((_ rotate_right 2) v238684)))
(let ((e238694 ((_ extract 12 12) e238689)))
(let ((e238695 (store a238688 ((_ sign_extend 8) e238694) ((_ zero_extend 3) e238692))))
(let ((e238696 (store a238688 ((_ zero_extend 6) v238684) ((_ sign_extend 3) v238685))))
(let ((e238697 (select a238688 ((_ extract 8 0) e238689))))
(let ((e238698 (store a238688 ((_ zero_extend 8) e238694) ((_ zero_extend 3) e238691))))
(let ((e238699 (ite (bvsge ((_ zero_extend 10) v238685) e238690)(_ bv1 1) (_ bv0 1))))
(let ((e238700 (bvsub ((_ sign_extend 11) e238692) e238689)))
(let ((e238701 (ite (bvsge e238697 ((_ zero_extend 3) e238693))(_ bv1 1) (_ bv0 1))))
(let ((e238702 ((_ sign_extend 9) e238694)))
(let ((e238703 (bvsdiv ((_ sign_extend 11) v238686) e238700)))
(let ((e238704 (ite (bvuge e238691 e238693)(_ bv1 1) (_ bv0 1))))
(let ((e238705 (bvcomp v238684 ((_ zero_extend 2) e238694))))
(let ((e238706 (bvule v238685 ((_ sign_extend 2) e238701))))
(let ((e238707 (bvslt e238692 e238691)))
(let ((e238708 (bvule v238686 e238691)))
(let ((e238709 (bvult e238697 ((_ zero_extend 3) v238685))))
(let ((e238710 (bvule e238690 ((_ sign_extend 10) v238684))))
(let ((e238711 (bvugt e238693 e238693)))
(let ((e238712 (distinct ((_ sign_extend 2) e238705) e238693)))
(let ((e238713 (distinct ((_ zero_extend 13) e238704) e238700)))
(let ((e238714 (= e238702 ((_ zero_extend 7) e238691))))
(let ((e238715 (bvsle ((_ sign_extend 2) e238705) e238692)))
(let ((e238716 (bvugt v238684 ((_ zero_extend 2) e238705))))
(let ((e238717 (bvslt v238686 ((_ zero_extend 2) e238701))))
(let ((e238718 (bvule e238704 e238694)))
(let ((e238719 (bvsgt ((_ zero_extend 2) e238699) v238686)))
(let ((e238720 (bvsgt e238702 ((_ zero_extend 9) e238705))))
(let ((e238721 (bvuge ((_ sign_extend 2) e238704) e238693)))
(let ((e238722 (bvsgt ((_ sign_extend 10) v238686) e238690)))
(let ((e238723 (bvult v238686 e238692)))
(let ((e238724 (bvuge v238686 v238685)))
(let ((e238725 (bvult e238704 e238699)))
(let ((e238726 (bvsge e238689 ((_ sign_extend 13) e238699))))
(let ((e238727 (bvule e238701 e238699)))
(let ((e238728 (bvule ((_ sign_extend 2) e238701) e238691)))
(let ((e238729 (bvule e238694 e238701)))
(let ((e238730 (bvule v238685 e238693)))
(let ((e238731 (bvsge ((_ sign_extend 2) e238705) e238693)))
(let ((e238732 (bvsge e238697 ((_ sign_extend 5) e238704))))
(let ((e238733 (bvsgt ((_ zero_extend 2) e238701) e238693)))
(let ((e238734 (= e238689 ((_ zero_extend 11) v238685))))
(let ((e238735 (bvugt ((_ zero_extend 7) e238697) e238690)))
(let ((e238736 (bvuge ((_ sign_extend 2) e238701) v238685)))
(let ((e238737 (bvule e238701 e238705)))
(let ((e238738 (bvsgt e238700 ((_ sign_extend 1) e238690))))
(let ((e238739 (bvslt ((_ sign_extend 13) e238704) e238689)))
(let ((e238740 (bvuge e238703 ((_ sign_extend 13) e238699))))
(let ((e238741 (=> e238716 e238719)))
(let ((e238742 (or e238740 e238721)))
(let ((e238743 (or e238713 e238734)))
(let ((e238744 (ite e238708 e238725 e238708)))
(let ((e238745 (= e238736 e238729)))
(let ((e238746 (ite e238726 e238717 e238706)))
(let ((e238747 (not e238709)))
(let ((e238748 (or e238707 e238732)))
(let ((e238749 (xor e238748 e238711)))
(let ((e238750 (or e238747 e238731)))
(let ((e238751 (and e238720 e238724)))
(let ((e238752 (and e238749 e238738)))
(let ((e238753 (xor e238735 e238741)))
(let ((e238754 (or e238744 e238753)))
(let ((e238755 (xor e238751 e238710)))
(let ((e238756 (or e238714 e238755)))
(let ((e238757 (xor e238742 e238727)))
(let ((e238758 (or e238722 e238715)))
(let ((e238759 (and e238758 e238718)))
(let ((e238760 (and e238757 e238737)))
(let ((e238761 (not e238759)))
(let ((e238762 (ite e238745 e238756 e238712)))
(let ((e238763 (not e238762)))
(let ((e238764 (not e238754)))
(let ((e238765 (xor e238733 e238750)))
(let ((e238766 (= e238743 e238730)))
(let ((e238767 (ite e238728 e238746 e238764)))
(let ((e238768 (not e238766)))
(let ((e238769 (xor e238765 e238765)))
(let ((e238770 (ite e238761 e238767 e238769)))
(let ((e238771 (and e238760 e238763)))
(let ((e238772 (or e238723 e238768)))
(let ((e238773 (=> e238739 e238771)))
(let ((e238774 (= e238772 e238752)))
(let ((e238775 (not e238774)))
(let ((e238776 (= e238770 e238770)))
(let ((e238777 (= e238773 e238776)))
(let ((e238778 (= e238775 e238775)))
(let ((e238779 (= e238777 e238778)))
e238779
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(pop 1)
